nLab Thomas Streicher

• website

Selected writings

On categorical semantics of (dependent) type theory (and proving an initiality conjecture in Ch. 4), see at categorical model of dependent types:

• Thomas Streicher, Semantics of type theory – Correctness, completeness and independence results, Progress in Theoretical Computer Science, Birkhäuser Boston (1991) [ISBN:0-8176-3594-7, doi:10.1007/978-1-4612-0433-6]

On intensional type theory:

• Thomas Streicher, Investigations into Intensional Type Theory, Habilitation Thesis, Darmstadt (1993) [pdf, pdf]

Introducing the homotopy type theory-interpretation of identity types (the “groupoid model”)

• Martin Hofmann, Thomas Streicher, The groupoid model refutes uniqueness of identity proofs, Proceedings Ninth Annual IEEE Symposium on Logic in Computer Science (1994) [doi:10.1109/LICS.1994.316071]

and introducing what came to be known the univalence axiom (under the name “universe extensionality”):

• Martin Hofmann, Thomas Streicher The groupoid interpretation of type theory, in: Giovanni Sambin et al. (eds.), Twenty-five years of constructive type theory, Proceedings of a congress, Venice, Italy, October 19-21, 1995. Oxford: Clarendon Press. Oxf. Logic Guides. 36 (1998) 83-111 [ISBN:9780198501275, ps.gz, pdf]

  see also:

  Ethan Lewis, Max Bohnet, The groupoid model of type theory, seminar notes (2017) [pdf, pdf]

On category theory and categorical logic:

• Thomas Streicher, Introduction to Category Theory and Categorical Logic (2003) [pdf, pdf]

On denotational semantics and domain theory for functional programming languages:

• Thomas Streicher, Domain-Theoretic Foundations of Functional Programming, World Scientific (2006) [pdf, doi:10.1142/6284]

On first-order set theory and categorical logic:

• Steve Awodey, Carsten Butz, Alex Simpson, Thomas Streicher, Relating first-order set theories, toposes and categories of classes, Annals of Pure and Applied Logic 165 2 (2014) 428-502 [doi:10.1016/j.apal.2013.06.004]

On fibered categories following Jean Bénabou:

• Thomas Streicher, Fibred Categories à la Jean Bénabou, [arXiv:1801.02927]

A 2-comonad characterizing Grothendieck fibrations:

• Jacopo Emmenegger, Luca Mesiti, Giuseppe Rosolini, Thomas Streicher, A comonad for Grothendieck fibrations [arXiv:2305.01474]

category: people